% Inference and checking predicates.
% $Id: rules.pl 3 2009-09-05 16:54:00Z colorachos $

:-asserta(pred(isA)).

event_pr(N,C,R,A):-
 write('..event:['),write(N),write(']'),nl,
 call(C),
 retractall(R),
 asserta(A).

ifthen(C,A):-
   call(C),
   not(A),
   write('....fired:['),write(C),write('/'),write(A),write(']'),nl,
   asserta(onefired),
   asserta(A).

fcha:-
 retractall(onefired),
 forall(
   rule(R,C,A),
   (write('..testing:'),write(R),nl,
    ((ifthen(C,A),asserta(fact(fired(R))));true)
   )
   ),
   onefired,
   !,
   fcha.
fcha.   

events:-
 forall(
   call(rulev(N,C,R,A)),
   event_pr(N,C,R,A)
   ).

unique(P):-
 write('...checking:'),write(P),nl,
 Pred =.. [P,X,Y],
 Pred2 =.. [P,X,Z],
 Fact =.. [fact,Pred],
 Fact2 =.. [fact,Pred2],
 forall(
   call(Fact),
   forall(
    call(Fact2),
     (not(Y==Z),write('error(not unique):'),
      write('pred['),write(P),write('] subject['),
      write(X),write('] val1['),
      write(Y),write('] val2['),write(Z),write(']'),nl,fail)
   )
  ).
unique(_).

contradiction(P):-
 write('...checking:'),write(P),nl,
 Pred =.. [P,X,true],
 Pred2 =.. [P,X,fail],
 Fact =.. [fact,Pred],
 Fact2 =.. [fact,Pred2],
 forall(
   call(Fact),
   (
    call(Fact2),
    write('error(contradiction):'),
    write('pred['),write(P),write('],subj['),write(X),write(']'),nl
   )
 ).
contradiction(_).

unviolated(I,C,A):-
 write('...checking:'),write(I),nl,
 forall(
  call(C),
  (
   not(call(A)),
   write('error(invariant violated):['),write(I),write('].'),
   write('condition:['),write(C),write(']'),
   nl
  )
 ).
unviolated(_,_,_).

neverfired(R):-
 write('...checking:'),write(R),nl,
 not(fact(fired(R))),
 write('warning(never fired):['),write(R),write('].'),nl.
neverfired(_).

frame_completion(FR):-
 write('...checking:'),write(FR),nl,
 Fact =.. [FR,N,_],
 Fact2 =.. [event, Fact],
 call(Fact2),
 forall(
   call(frame(FR,FA)),
   (
    FactCh =.. [FA,N,_],
    not(fact(FactCh)),
    write('warning(frame incomplete):['),write(FactCh),nl
   )
 ).
frame_completion(_).

check:-
  write('checking for duplicity'),nl,
  write('----------------------'),nl,
 forall(
   (pred(P),fact(isA(P,uniquep))),
   unique(P)
   ),
  write('ok!'),nl,
  write('checking for contradictions'),nl,
  write('---------------------------'),nl,
 forall(
   pred(P),
   contradiction(P)
   ),
  write('ok!'),nl,
  write('checking invariants'),nl,
  write('-------------------'),nl,
 forall(
   invariant(I,C,A),
   unviolated(I,C,A)
   ),
  write('ok!'),nl,
  write('checking for never-fired rules'),nl,
  write('------------------------------'),nl,
 forall(
   rule(R,_,_),
   neverfired(R)
   ),
  write('ok!'),nl,
  write('checking for frame completion'),nl,
  write('----------------------------'),nl,
 (
  frames_checked;
  (
   asserta(fact(frames_checked)),
   forall(
    (
     frame(FR,_),
     not(fact(frame_checked(FR)))
    ),
    (
     asserta(fact(frame_checked(FR))),
     frame_completion(FR)
    )
   )
  )
 ),
 write('ok!'),nl
  .

load:-consult('model.kb'),consult('facts.kb').
reset:-
 retractall(fact(_)),
 retractall(pred(_)),
 retractall(event(_)),
 retractall(rule(_,_,_)),
 retractall(rulev(_,_,_,_)),
 retractall(frame(_,_)),
 retractall(frames_checked),
 retractall(frame_checked(_)),
 retractall(invariant(_,_,_)).
